Propositions as Types

自然演繹の証明系における含意の関する規則が、関数のラムダ抽象と適用に関する規則と正確に対応しているという事実は、Curry-Howard isomorphism(カリー=ハワード同型)の一例であり、proposition-as-types(型としての命題)パラダイムとして知られている。